DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2016.25

Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis

Authors: Jean-Louis Krivine

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract

This paper is about the bar recursion operator in the context of classical realizability. The pioneering work of Berardi, Bezem, Coquand was enhanced by Berger and Oliva. Then Streicher has shown, by means of their bar recursion operator, that the realizability models of ZF, obtained from usual models of lambda-calculus (Scott domains, coherent spaces, ...), satisfy the axiom of dependent choice. We give a proof of this result, using the tools of classical realizability. Moreover, we show that these realizability models satisfy the well ordering of R and the continuum hypothesis. These formulas are therefore realized by closed lambda_c-terms. This new result allows to obtain programs from proofs of arithmetical formulas using all these axioms.

Cite as

Jean-Louis Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 25:1-25:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{krivine:LIPIcs.CSL.2016.25,
  author =	{Krivine, Jean-Louis},
  title =	{{Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{25:1--25:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.25},
  URN =		{urn:nbn:de:0030-drops-65650},
  doi =		{10.4230/LIPIcs.CSL.2016.25},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.146

On the Structure of Classical Realizability Models of ZF

Authors: Jean-Louis Krivine

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract

The technique of classical realizability is an extension of the method of forcing; it permits to extend the Curry-Howard correspondence between proofs and programs, to Zermelo-Fraenkel set theory and to build new models of ZF, called realizability models. The structure of these models is, in general, much more complicated than that of the particular case of forcing models. We show here that the class of constructible sets of any realizability model is an elementary extension of the constructibles of the ground model (a trivial fact in the case of forcing, since these classes are identical). By Shoenfield absoluteness theorem, it follows that every true Sigma^1_3 formula is realized by a closed lambda_c-term.

Cite as

Jean-Louis Krivine. On the Structure of Classical Realizability Models of ZF. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 146-161, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{krivine:LIPIcs.TYPES.2014.146,
  author =	{Krivine, Jean-Louis},
  title =	{{On the Structure of Classical Realizability Models of ZF}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{146--161},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.146},
  URN =		{urn:nbn:de:0030-drops-54953},
  doi =		{10.4230/LIPIcs.TYPES.2014.146},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}

Search Results

Documents authored by Krivine, Jean-Louis

Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis

Abstract

Cite as

On the Structure of Classical Realizability Models of ZF

Abstract

Cite as

Thanks for your feedback!

Could not send message